Nuprl Lemma : det_ideal_defines_eqv
13,42
postcript
pdf
r
:CRng,
a
:Ideal(
r
){i},
d
:detach_fun(|
r
|;
a
). EquivRel(|
r
|;
u
,
v
.
(
d
(
u
+
r
(-
r
(
v
)))))
latex
Up
rings
1
Definitions of Statement
Rng
,
CRng
,
Ideal(
r
){i}
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
x
,
y
.
t
(
x
;
y
)
,
,
P
Q
,
x
f
y
,
P
Q
,
True
,
T
,
False
,
Rng
,
Ideal(
r
){i}
,
CRng
,
{
T
}
,
detach_fun(
T
;
A
)
,
x
(
s1
,
s2
)
,
P
Q
,
A
,
P
Q
,
Dec(
P
)
,
XM
Lemmas
crng
wf
,
ideal
wf
,
rng
car
wf
,
detach
fun
wf
,
detach
fun
properties
,
squash
wf
,
rng
minus
wf
,
rng
plus
wf
,
assert
wf
,
equiv
rel
functionality
wrt
iff
,
squash
thru
equiv
rel
,
ideal
defines
eqv
,
ideal
p
wf
origin